Lemma apply_premise:
  forall p q: Prop, (p->q) -> p -> q.
Proof.
  intros p q H1 H2.
  apply H1.
  assumption.
Qed.